ePMC

Benchmark
Model:consensus v.1 (MDP)
Parameter(s)N = 4, K = 4
Property:disagree (prob-reach)
Invocation (default)
java -Xms10240m -Xmx10240m -jar ./root/epmc-standard.jar check --model-input-files consensus.4.prism --model-input-type prism --property-input-files consensus.props --property-input-names disagree --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const K=4
Execution
Walltime:11.484796285629272s
Return code:0
Relative Error:5.52340564152121e-05
Log
assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property disagree
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 16499 16498
build-model-done 43136 1
iterating
iterating-progress-unbounded 798 0.01914609466511378 1
iterating-progress-unbounded 1687 0.002888524517598791 2
iterating-progress-unbounded 2574 6.490218880098335E-4 3
iterating-progress-unbounded 3462 1.4847147543751624E-4 4
iterating-progress-unbounded 4349 3.320446305838085E-5 5
iterating-progress-unbounded 5237 7.123241592866622E-6 6
iterating-progress-unbounded 6124 1.5011148394216882E-6 7
iterating-done 6741 7
model-checking-done 10
command-check-result-is 0.15606444343964274 disagree